n:. nth_tl(n;nil) ~ nil 

latex

Definitions	tl(l), Unit, P  Q, P & Q, P  Q, T, , b, b, True, Prop, nth_tl(n;as), AB, A, False, ij, P  Q, x:A. B(x), t  T, , ij, i<j
Lemmas	nat wf, nat properties, ge wf, bnot wf, assert wf, lt int wf, le wf, bool wf, le int wf, assert of lt int, bnot of le int, true wf, squash wf, eqff to assert, iff transitivity, assert of le int, eqtt to assert